Inference at * 2 0 1 2 1 
Iof proof for Lemma multiply nat wf:



1. i : 
2. 0  0 
  0  (i * 0) 

latex

 by ((Thin (-1)) 
CollapseTHEN (AddHiddenLabel `basecase`)) 

latex

C1: .....basecase..... NILNIL

C1: 1. i : 
C1:   0  (i * 0)
C.

Definitions

n * m, A  B, #$n, i  j ,